﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;

using SimpleIR;

namespace PInfoModel
{
	/// <summary>
	/// The complete information (all call contexts) for a given method.
	/// </summary>
	public sealed class CompleteAnalysisInfoMethod
	{
		/// <summary>
		/// The invoke identity of this context state.
		/// </summary>
		private readonly IRInvokeIdentity m_invokeid;

		/// <summary>
		/// The summary (merge of all in and out states) input and output states for this method.
		/// </summary>
		private PIModel m_summaryinstate;
		private PIModel m_summaryoutstate;

		/// <summary>
		/// The list of all call contexts associated with this method.
		/// </summary>
		private readonly List<CompleteAnalysisInfoMethodContext> m_allcallcontexts;

		/// <summary>
		/// Map from external ref names in the summary states to the set of all the names in the individual contexts.
		/// </summary>
		private Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>> m_individualcontextstosummaymapext;

		/// <summary>
		/// Map from ids in the summary states to the set of all the ids in the individual contexts.
		/// </summary>
		private Dictionary<int, HashSet<int>> m_individualcontextstosummaymapid;

		/// <summary>
		/// Map from loop header ids to a tuple of summary models over all call contexts: at entry to the head block and immediately after the merge for the back flow edge.
		/// </summary>
		private readonly Dictionary<long, PIModel> m_loopidtobeforeafterbodymap;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.m_invokeid != null);
			Contract.Invariant(this.m_allcallcontexts != null);
		}

		public CompleteAnalysisInfoMethod(IRInvokeIdentity iiv, List<CompleteAnalysisInfoMethodContext> allcctxts, Dictionary<long, PIModel> loopidtobeforeafterbodymap)
		{
			this.m_invokeid = iiv;
			this.m_allcallcontexts = allcctxts;
			this.m_loopidtobeforeafterbodymap = loopidtobeforeafterbodymap;
		}

		public void FinalizeSummaryInfo(PIModel summaryin, PIModel summaryout, Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>> erremap, Dictionary<int, HashSet<int>> idremap)
		{
			this.m_summaryinstate = summaryin;
			this.m_summaryoutstate = summaryout;

			this.m_individualcontextstosummaymapext = erremap;
			this.m_individualcontextstosummaymapid = idremap;
		}

		/// <summary>
		/// The invoke identity of this context state.
		/// </summary>
		public IRInvokeIdentity InvokeID
		{ get { return this.m_invokeid; } }

		/// <summary>
		/// The summary (merge of all in states) input and output states for this method.
		/// </summary>
		public PIModel SummaryInState
		{ get { return this.m_summaryinstate; } }

		/// <summary>
		/// The summary (merge of all out states) input and output states for this method.
		/// </summary>
		public PIModel SummaryOutState
		{ get { return this.m_summaryoutstate; } }

		/// <summary>
		/// The list of all call contexts associated with this method.
		/// </summary>
		public List<CompleteAnalysisInfoMethodContext> AllCallContexts
		{ get { return this.m_allcallcontexts; } }

		/// <summary>
		/// Map from external ref names in the summary states to the set of all the names in the individual contexts.
		/// </summary>
		public Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>> IndividualContextsToSummayMapExt
		{ get { return this.m_individualcontextstosummaymapext; } }

		/// <summary>
		/// Map from ids in the summary states to the set of all the ids in the individual contexts.
		/// </summary>
		public Dictionary<int, HashSet<int>> IndividualContextsToSummayMapID
		{ get { return this.m_individualcontextstosummaymapid; } }

		/// <summary>
		/// Map from loop header ids to a tuple of models: at entry to the head block and immediately after the merge for the back flow edge.
		/// </summary>
		public Dictionary<long, PIModel> LoopIDToBeforeAfterBodyMap
		{ get { return this.m_loopidtobeforeafterbodymap; } }
	}
}
